\begin{tabbing}
$\forall$${\it es}$:ES, $A$, $V$:Type, $i$:Id, ${\it knd}$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\\[0ex]($\forall$$e$:E.
\\[0ex](loc($e$) = $i$) $\Rightarrow$ (kind($e$) = ${\it knd}$) $\Rightarrow$ ((valtype($e$) $\subseteq$r $V$) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]($\uparrow$($e$ $\in_{b}$ es{-}trigger(${\it es}$;$i$;${\it knd}$;${\it ds}$;$f$)))
\\[0ex]$\Leftarrow\!\Rightarrow$ (loc($e$) = $i$ \& kind($e$) = ${\it knd}$ \& ($\uparrow$isl($f$((state when $e$),val($e$))))))
\-
\end{tabbing}